*****∧I INDUCTION;

1 (∀v.∃w.(nil APP v)=w∧∀u.((¬(u=nil)∧∀v.∃w.(cdr u APP v)=w)⊃∀v.∃w.(u APP v)=w))⊃∀u v.∃w.(u APP v)=w  

*****∀E APPEND nil,v;

2 (nil APP v)=IF nil=nil THEN v ELSE CONS(CAR nil,CDR nil APP v)  

*****DISTRIB;

3 (nil APP v)=IF nil=nil THEN v ELSE CONS(CAR nil,CDR nil APP v)≡IF nil=nil THEN (nil APP v)=v ELSE (nil APP v)=%
CONS(CAR nil,CDR nil APP v)  

*****TAUTEQ nil=nil ;

4 nil=nil  

*****TAUT (nil APP v)=v ↑↑↑:↑;

5 (nil APP v)=v  

*****∃I ↑ v←w OCC ((2));

6 ∃w.(nil APP v)=w  

*****∀I ↑ v;

7 ∀v.∃w.(nil APP v)=w  

*****∀E APPEND u,v;

8 (u APP v)=IF u=nil THEN v ELSE CONS(CAR u,CDR u APP v)  

*****DISTRIB;

9 (u APP v)=IF u=nil THEN v ELSE CONS(CAR u,CDR u APP v)≡IF u=nil THEN (u APP v)=v ELSE (u APP v)=CONS(CAR u,CDR%
 u APP v)  

*****ASSUME ¬(u=nil);

10 ¬(u=nil)  (10)

*****TAUT (u APP v)=CONS(CAR u,CDR u APP v) ↑↑↑:↑;

11 (u APP v)=CONS(CAR u,CDR u APP v)  (10)

*****ASSUME ∀v.∃w.(cdr u APP v)=w;

12 ∀v.∃w.(cdr u APP v)=w  (12)

*****∀E ↑ v;

13 ∃w.(cdr u APP v)=w  (12)

*****∃E ↑ w;

14 (cdr u APP v)=w  (14)

*****SUBSTR ↑ IN 11;

15 (u APP v)=CONS(CAR u,CDR u APP v)  (10 12)

*****∀E CDR u;

16 cdr u=CDR u  

*****SUBSTR ↑ IN ↑↑↑;

17 (CDR u APP v)=w  (14)

*****SUBSTR ↑ IN ↑↑↑;

18 (u APP v)=CONS(CAR u,w)  (10 12 14)

*****∀E CAR u;

19 car u=CAR u  

*****SUBST ↑ IN ↑↑;

20 (u APP v)=CONS(car u,w)  (10 12 14)

*****∀E CONS car u,w;

21 cons(car u,w)=CONS(car u,w)  

*****SUBST ↑ IN ↑↑;

22 (u APP v)=cons(car u,w)  (10 12 14)

*****∃I ↑ cons(car u,w)←w;

23 ∃w.(u APP v)=w  (10 12)

*****∀I ↑ v;

24 ∀v.∃w.(u APP v)=w  (10 12)

*****⊃I 12⊃↑;

25 ∀v.∃w.(cdr u APP v)=w⊃∀v.∃w.(u APP v)=w  (10)

*****⊃I 10⊃↑;

26 ¬(u=nil)⊃(∀v.∃w.(cdr u APP v)=w⊃∀v.∃w.(u APP v)=w)  

*****TAUT (¬(u=nil)∧∀v.∃w.(cdr u APP v)=w)⊃∀v.∃w.(u APP v)=w ↑;

27 (¬(u=nil)∧∀v.∃w.(cdr u APP v)=w)⊃∀v.∃w.(u APP v)=w  

*****∀I ↑ u;

28 ∀u.((¬(u=nil)∧∀v.∃w.(cdr u APP v)=w)⊃∀v.∃w.(u APP v)=w)  

*****TAUT ∀u v.∃w.(u APP v)=w 1,7,↑;

29 ∀u v.∃w.(u APP v)=w  

*****∀E APPEND2 u,v;

30 (u app v)=IF ∃w.(u APP v)=w THEN u APP v ELSE nil  

*****DISTRIB;

31 (u app v)=IF ∃w.(u APP v)=w THEN u APP v ELSE nil≡IF ∃w.(u APP v)=w THEN (u app v)=(u APP v) ELSE (u app v)=n%
il  

*****∀E ↑↑↑ u,v;

32 ∃w.(u APP v)=w  

*****TAUT (u app v)=(u APP v) ↑↑↑:↑;

33 (u app v)=(u APP v)  

*****∀I ↑ u v;

34 ∀u v.(u app v)=(u APP v)  

*****∀E ↑ cdr u,v;

35 (cdr u app v)=(cdr u APP v)  

*****∀E APPEND1 u,v;

36 (u APP v)=IF u=nil THEN v ELSE CONS(CAR u,CDR u APP v)  

*****∀E CDR u;

37 cdr u=CDR u  

*****SUBSTR ↑ IN ↑↑↑ OCC 2;

38 (cdr u app v)=(CDR u APP v)  

*****SUBST ↑ IN ↑↑↑;

39 (u APP v)=IF u=nil THEN v ELSE CONS(CAR u,cdr u app v)  

*****∀E CAR u;

40 car u=CAR u  

*****SUBST ↑ IN ↑↑;

41 (u APP v)=IF u=nil THEN v ELSE CONS(car u,cdr u app v)  

*****∀E CONS car u,cdr u app v;

42 cons(car u,cdr u app v)=CONS(car u,cdr u app v)  

*****SUBST ↑ IN ↑↑;

43 (u APP v)=IF u=nil THEN v ELSE cons(car u,cdr u app v)  

*****SUBST 33 IN ↑;

44 (u app v)=IF u=nil THEN v ELSE cons(car u,cdr u app v)  

*****∀I ↑ u v;

45 ∀u v.(u app v)=IF u=nil THEN v ELSE cons(car u,cdr u app v)